/*------ Politics 2.0----------------------+
|														|
|		Mohamed Aboelkheir				|
|		Samuele Tosatto						|
|														|
+-------------------------------------------+
	DESCRIPTION

	This model gives a general view about the concept of Politic 2.0.
	We modeled 
	User, Citizen, Governor, Party.
	MembReq models the fact that one citizen can perform a request to join a party.
	ReqVote models the fact that every member of a Party can vote for the acceptance (or reject) of a request.

	We modeled also the fact that a member request is Accepted if and only if the number of votes=YES are greater than 50% of number of member on that party
	and symmetrically a member request is rejected if and only if the number of votes=NO are greater than 50%..
	A member request results pending otherwise.

	Note also that when a Member request is Accepted, the citizen is automatically a member of a party

	This Alloy is static, and we think that is sufficient to give a general idea and description about the system that we will implement.

*/


module Politics2

sig UString {}
sig posInt  { value: Int} {value > 0}

/*
Describes the account information of a user
*/
abstract sig  User 
{
	id: one posInt,
	username:one UString,
	password:one UString,
	firstname:one UString,
	lastname:one UString,
	email:one UString,
	phone:lone UString,
}
//{username != email}

/*
Describes a registered citizen in the system
*/
sig Citizen extends User 
{
	//Every citizen could perform at maximum one request to become a member of a party
	membrequest: lone MembRequest,
	//Every citizen can be  member of at maximum one party
	party: lone Party
}
{
	//Every citizen can send a request or be already a member of a party. When a request is accepted then the citizen is also  a member
	membrequest=none or party = none or (membrequest.status = Accepted and party=membrequest.party)
	//NOTE that is not true that for every citizen that is member of a party must have also a request for that party, in general we consider that some citizen could be member of a party without any request
}

/*
This signature describes a party
*/
sig Party
{
	id:one posInt,
	name:one UString,
	symbol:one Symbol,
	program:one UString,
	//This is the set of the citizen that are already member of this party: note that every party, must have at least one member
	members: some Citizen
}
sig Symbol{

}
/*
This signature describes a governor
*/
sig Governor extends User
{
	//We assume for semplicity that the information of a candidacy is unique (there are no multiple candidacy window)
	candidacyBegin: one posInt,
	candidacyEnd: one posInt,
	
	ElectionDays: some posInt
}
{ 
	//We also assume that there is only one governor. This assumption is obvisully stricht but there is the possibility to avoid it in the next version of the software
	#Governor = 1
	and candidacyBegin.value <= candidacyEnd.value
}

/*
This signature model a request to join a party
*/
sig MembRequest 
{
	//status describes if the request is accepted, rejected yes or it is not decided yet (Pending)
	status: one Status,
	//this is the party where the citizen is applying for
	party: one Party,
	//the citizen is who is requiring to apply
	citizen: one Citizen
}

enum Status {Accepted, Rejected, Pending}

/*
This signature model the vote that each member of a party could express to a request of joining
*/
abstract sig ReqVote 
{
	//this is the citizen that is expressing his opinion
	citizen: one Citizen,
	//this is the member request in object
	membrequest: one MembRequest,
	//this is the time when the vote is expressed (it should be during the candidacy window)
	time: one posInt
}
{
	//constraint on the time of the vote
	 time.value <= Governor. candidacyEnd.value and time.value >= Governor.candidacyBegin.value and citizen != membrequest.citizen
}
//This is a positive vote (means that the citizen accepted the member request)
sig PositiveVote extends ReqVote{

}
//this is a negative vote (means that the citizen would reject the member request)
sig NegativeVote extends ReqVote{

}

/*
This costraint impose that a request is Accepted If and only If the number of positive votes on the request are greater than 50% of the #of member of the party
and symmetrically  a request is Rejected If and only If the number of positive votes on the request are greater than 50% of the #of the member of the party
*/
fact AcceptedIfRejectedIf {
	all r : MembRequest | (r.status = Accepted iff ( (sum pv : PositiveVote | pv.membrequest.citizen = r.citizen implies 2 else 0)  > (sum c: Citizen | c.party = r.party implies 1 else 0)-1/*we should subtract the new member on this counting*/)) and
	all r : MembRequest | (r.status = Rejected iff( (sum pv : NegativeVote | pv.membrequest.citizen = r.citizen implies 2 else 0)  > (sum c: Citizen | c.party = r.party implies 1 else 0)))
}

/*
The request of vote cabn be performed only once by a citizen for the same request (any request is unique for the citizen)
*/
fact RequestOnlyOne{
	all disj r1,r2 : ReqVote  | r1.citizen = r2.citizen implies r1.membrequest.citizen != r2.membrequest.citizen 
}

/*
This signature means the vote expressed during the election day
*/
sig ElectionVote
{
	//citizen who expressed the vote
	citizen: one Citizen,
	//for wich party
	party: one Party,
	//with this preferences list
	pref_one: one Citizen,
	pref_two: lone Citizen,
	pref_three: lone Citizen,
	date: one posInt
}
{
	// the First three conditions makes sure that the choices are different -- the fourth one to make sure that if the second choice is none, then the third is none.
	 pref_one & pref_two = none and pref_one & pref_three = none and pref_three & pref_two = none
	and #pref_two >= #pref_three
	and pref_one + pref_two + pref_three in party.members
	and date in Governor.ElectionDays
}


//-------------------------------NO DUPLICATE Objects of the entities------------------------

fact NoDuplicates{
	no disj p1,p2:posInt| p1.value =p2.value
	no disj u1,u2:User| (u1.id=u2.id or u1.email = u2.email or u1.username = u2.username)
	no disj p1, p2:Party| (p1.id = p2.id or p1.name = p2.name or p1.symbol = p2.symbol)
	no disj rv1, rv2:MembRequest | (rv1. citizen = rv2.citizen and rv1.membrequest = rv2.membrequest)
	no disj ev1, ev2:MembRequest | (ev1.citizen = ev2.citizen)
}

//Check if a relation between citizen and user or unique.
fact MembRequestCoherency {
	all r: MembRequest | all c: Citizen | c=r.citizen iff r=c.membrequest
}

//Only members of the same party can vote for the new membership requests.
fact OnlyPartyMemberVotes {
 	all rv:ReqVote | rv.citizen.party = ReqVote.membrequest.party
}

fact MembersIncludedinPartyListOfMembers {
	all p:Party | all c:Citizen | c.party = p iff c in p.members
}

fact ElectionVoteUniqueForCitizen{
	all disj e1,e2:ElectionVote | e1.citizen!=e2.citizen
}

fact SymbolForParties{
	#Party = #Symbol
}

pred show()
{	
	//(sum r : MembRequest | r.status=-Accepted implies 1 else 0 )>=1
	(sum r : MembRequest | r.status=Rejected implies 1 else 0 )>=1
	#Party >=2
	some p:Party | #(p.members) >2
	#ElectionVote>=1
}

run show for 8
